\begin{tabbing}
$\forall$$T$:Type, ${\it eq}$:EqDecider($T$), ${\it es}$:event\_system\{i:l\}, $x$:Id, $e$:\{\=$e$:es{-}E(${\it es}$)$\mid$ \+
\\[0ex]es{-}dtype(${\it es}$; loc($e$); $x$; $T$)\} .
\-\\[0ex]($\uparrow$$x$ changed before $e$)
\\[0ex]$\Rightarrow$ \=(es{-}locl(${\it es}$; (last change to $x$ before $e$); $e$)\+
\\[0ex]c$\wedge$ \=(@(last change to $x$ before $e$)($x$$\rightarrow$es{-}when(${\it es}$; $x$; $e$))\+
\\[0ex]$\wedge$ $\forall$${\it e''}$$\in$((last change to $x$ before $e$),$e$].es{-}when(${\it es}$; $x$; ${\it e''}$) = es{-}when(${\it es}$; $x$; $e$) $\in$ $T$))
\-\-
\end{tabbing}